1: | app(nil,YS) | → YS | |
2: | app(cons(X,XS),YS) | → cons(X,n__app(activate(XS),YS)) | |
3: | from(X) | → cons(X,n__from(n__s(X))) | |
4: | zWadr(nil,YS) | → nil | |
5: | zWadr(XS,nil) | → nil | |
6: | zWadr(cons(X,XS),cons(Y,YS)) | → cons(app(Y,cons(X,n__nil)),n__zWadr(activate(XS),activate(YS))) | |
7: | prefix(L) | → cons(nil,n__zWadr(L,n__prefix(L))) | |
8: | app(X1,X2) | → n__app(X1,X2) | |
9: | from(X) | → n__from(X) | |
10: | s(X) | → n__s(X) | |
11: | nil | → n__nil | |
12: | zWadr(X1,X2) | → n__zWadr(X1,X2) | |
13: | prefix(X) | → n__prefix(X) | |
14: | activate(n__app(X1,X2)) | → app(activate(X1),activate(X2)) | |
15: | activate(n__from(X)) | → from(activate(X)) | |
16: | activate(n__s(X)) | → s(activate(X)) | |
17: | activate(n__nil) | → nil | |
18: | activate(n__zWadr(X1,X2)) | → zWadr(activate(X1),activate(X2)) | |
19: | activate(n__prefix(X)) | → prefix(activate(X)) | |
20: | activate(X) | → X | |
21: | APP(cons(X,XS),YS) | → ACTIVATE(XS) | |
22: | ZWADR(cons(X,XS),cons(Y,YS)) | → APP(Y,cons(X,n__nil)) | |
23: | ZWADR(cons(X,XS),cons(Y,YS)) | → ACTIVATE(XS) | |
24: | ZWADR(cons(X,XS),cons(Y,YS)) | → ACTIVATE(YS) | |
25: | PREFIX(L) | → NIL | |
26: | ACTIVATE(n__app(X1,X2)) | → APP(activate(X1),activate(X2)) | |
27: | ACTIVATE(n__app(X1,X2)) | → ACTIVATE(X1) | |
28: | ACTIVATE(n__app(X1,X2)) | → ACTIVATE(X2) | |
29: | ACTIVATE(n__from(X)) | → FROM(activate(X)) | |
30: | ACTIVATE(n__from(X)) | → ACTIVATE(X) | |
31: | ACTIVATE(n__s(X)) | → S(activate(X)) | |
32: | ACTIVATE(n__s(X)) | → ACTIVATE(X) | |
33: | ACTIVATE(n__nil) | → NIL | |
34: | ACTIVATE(n__zWadr(X1,X2)) | → ZWADR(activate(X1),activate(X2)) | |
35: | ACTIVATE(n__zWadr(X1,X2)) | → ACTIVATE(X1) | |
36: | ACTIVATE(n__zWadr(X1,X2)) | → ACTIVATE(X2) | |
37: | ACTIVATE(n__prefix(X)) | → PREFIX(activate(X)) | |
38: | ACTIVATE(n__prefix(X)) | → ACTIVATE(X) | |